The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

D(t) → s(h)
D(constant) → h
D(b(x, y)) → b(D(x), D(y))
D(c(x, y)) → b(c(y, D(x)), c(x, D(y)))
D(m(x, y)) → m(D(x), D(y))
D(opp(x)) → opp(D(x))
D(div(x, y)) → m(div(D(x), y), div(c(x, D(y)), pow(y, 2)))
D(ln(x)) → div(D(x), x)
D(pow(x, y)) → b(c(c(y, pow(x, m(y, 1))), D(x)), c(c(pow(x, y), ln(x)), D(y)))
b(h, x) → x
b(x, h) → x
b(s(x), s(y)) → s(s(b(x, y)))
b(b(x, y), z) → b(x, b(y, z))

Rewrite Strategy: INNERMOST

(1) NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID) transformation)

The following defined symbols can occur below the 0th argument of b: b, D
The following defined symbols can occur below the 1th argument of b: b, D

Hence, the left-hand sides of the following rules are not basic-reachable and can be removed:
D(b(x, y)) → b(D(x), D(y))

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

D(constant) → h
D(c(x, y)) → b(c(y, D(x)), c(x, D(y)))
D(div(x, y)) → m(div(D(x), y), div(c(x, D(y)), pow(y, 2)))
D(ln(x)) → div(D(x), x)
b(b(x, y), z) → b(x, b(y, z))
D(t) → s(h)
D(m(x, y)) → m(D(x), D(y))
D(pow(x, y)) → b(c(c(y, pow(x, m(y, 1))), D(x)), c(c(pow(x, y), ln(x)), D(y)))
b(h, x) → x
b(x, h) → x
D(opp(x)) → opp(D(x))
b(s(x), s(y)) → s(s(b(x, y)))

Rewrite Strategy: INNERMOST

(3) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted Cpx (relative) TRS to CDT

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

D(constant) → h
D(c(z0, z1)) → b(c(z1, D(z0)), c(z0, D(z1)))
D(div(z0, z1)) → m(div(D(z0), z1), div(c(z0, D(z1)), pow(z1, 2)))
D(ln(z0)) → div(D(z0), z0)
D(t) → s(h)
D(m(z0, z1)) → m(D(z0), D(z1))
D(pow(z0, z1)) → b(c(c(z1, pow(z0, m(z1, 1))), D(z0)), c(c(pow(z0, z1), ln(z0)), D(z1)))
D(opp(z0)) → opp(D(z0))
b(b(z0, z1), z2) → b(z0, b(z1, z2))
b(h, z0) → z0
b(z0, h) → z0
b(s(z0), s(z1)) → s(s(b(z0, z1)))

Tuples:

D'(constant) → c1
D'(c(z0, z1)) → c2(B(c(z1, D(z0)), c(z0, D(z1))), D'(z0), D'(z1))
D'(div(z0, z1)) → c3(D'(z0), D'(z1))
D'(ln(z0)) → c4(D'(z0))
D'(t) → c5
D'(m(z0, z1)) → c6(D'(z0), D'(z1))
D'(pow(z0, z1)) → c7(B(c(c(z1, pow(z0, m(z1, 1))), D(z0)), c(c(pow(z0, z1), ln(z0)), D(z1))), D'(z0), D'(z1))
D'(opp(z0)) → c8(D'(z0))
B(b(z0, z1), z2) → c9(B(z0, b(z1, z2)), B(z1, z2))
B(h, z0) → c10
B(z0, h) → c11
B(s(z0), s(z1)) → c12(B(z0, z1))

S tuples:

D'(constant) → c1
D'(c(z0, z1)) → c2(B(c(z1, D(z0)), c(z0, D(z1))), D'(z0), D'(z1))
D'(div(z0, z1)) → c3(D'(z0), D'(z1))
D'(ln(z0)) → c4(D'(z0))
D'(t) → c5
D'(m(z0, z1)) → c6(D'(z0), D'(z1))
D'(pow(z0, z1)) → c7(B(c(c(z1, pow(z0, m(z1, 1))), D(z0)), c(c(pow(z0, z1), ln(z0)), D(z1))), D'(z0), D'(z1))
D'(opp(z0)) → c8(D'(z0))
B(b(z0, z1), z2) → c9(B(z0, b(z1, z2)), B(z1, z2))
B(h, z0) → c10
B(z0, h) → c11
B(s(z0), s(z1)) → c12(B(z0, z1))

K tuples:none
Defined Rule Symbols:

D, b

Defined Pair Symbols:

D', B

Compound Symbols:

c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 4 trailing nodes:

B(h, z0) → c10
B(z0, h) → c11
D'(t) → c5
D'(constant) → c1

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

D(constant) → h
D(c(z0, z1)) → b(c(z1, D(z0)), c(z0, D(z1)))
D(div(z0, z1)) → m(div(D(z0), z1), div(c(z0, D(z1)), pow(z1, 2)))
D(ln(z0)) → div(D(z0), z0)
D(t) → s(h)
D(m(z0, z1)) → m(D(z0), D(z1))
D(pow(z0, z1)) → b(c(c(z1, pow(z0, m(z1, 1))), D(z0)), c(c(pow(z0, z1), ln(z0)), D(z1)))
D(opp(z0)) → opp(D(z0))
b(b(z0, z1), z2) → b(z0, b(z1, z2))
b(h, z0) → z0
b(z0, h) → z0
b(s(z0), s(z1)) → s(s(b(z0, z1)))

Tuples:

D'(c(z0, z1)) → c2(B(c(z1, D(z0)), c(z0, D(z1))), D'(z0), D'(z1))
D'(div(z0, z1)) → c3(D'(z0), D'(z1))
D'(ln(z0)) → c4(D'(z0))
D'(m(z0, z1)) → c6(D'(z0), D'(z1))
D'(pow(z0, z1)) → c7(B(c(c(z1, pow(z0, m(z1, 1))), D(z0)), c(c(pow(z0, z1), ln(z0)), D(z1))), D'(z0), D'(z1))
D'(opp(z0)) → c8(D'(z0))
B(b(z0, z1), z2) → c9(B(z0, b(z1, z2)), B(z1, z2))
B(s(z0), s(z1)) → c12(B(z0, z1))

S tuples:

D'(c(z0, z1)) → c2(B(c(z1, D(z0)), c(z0, D(z1))), D'(z0), D'(z1))
D'(div(z0, z1)) → c3(D'(z0), D'(z1))
D'(ln(z0)) → c4(D'(z0))
D'(m(z0, z1)) → c6(D'(z0), D'(z1))
D'(pow(z0, z1)) → c7(B(c(c(z1, pow(z0, m(z1, 1))), D(z0)), c(c(pow(z0, z1), ln(z0)), D(z1))), D'(z0), D'(z1))
D'(opp(z0)) → c8(D'(z0))
B(b(z0, z1), z2) → c9(B(z0, b(z1, z2)), B(z1, z2))
B(s(z0), s(z1)) → c12(B(z0, z1))

K tuples:none
Defined Rule Symbols:

D, b

Defined Pair Symbols:

D', B

Compound Symbols:

c2, c3, c4, c6, c7, c8, c9, c12

(7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing tuple parts

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

D(constant) → h
D(c(z0, z1)) → b(c(z1, D(z0)), c(z0, D(z1)))
D(div(z0, z1)) → m(div(D(z0), z1), div(c(z0, D(z1)), pow(z1, 2)))
D(ln(z0)) → div(D(z0), z0)
D(t) → s(h)
D(m(z0, z1)) → m(D(z0), D(z1))
D(pow(z0, z1)) → b(c(c(z1, pow(z0, m(z1, 1))), D(z0)), c(c(pow(z0, z1), ln(z0)), D(z1)))
D(opp(z0)) → opp(D(z0))
b(b(z0, z1), z2) → b(z0, b(z1, z2))
b(h, z0) → z0
b(z0, h) → z0
b(s(z0), s(z1)) → s(s(b(z0, z1)))

Tuples:

D'(div(z0, z1)) → c3(D'(z0), D'(z1))
D'(ln(z0)) → c4(D'(z0))
D'(m(z0, z1)) → c6(D'(z0), D'(z1))
D'(opp(z0)) → c8(D'(z0))
B(b(z0, z1), z2) → c9(B(z0, b(z1, z2)), B(z1, z2))
B(s(z0), s(z1)) → c12(B(z0, z1))
D'(c(z0, z1)) → c2(D'(z0), D'(z1))
D'(pow(z0, z1)) → c7(D'(z0), D'(z1))

S tuples:

D'(div(z0, z1)) → c3(D'(z0), D'(z1))
D'(ln(z0)) → c4(D'(z0))
D'(m(z0, z1)) → c6(D'(z0), D'(z1))
D'(opp(z0)) → c8(D'(z0))
B(b(z0, z1), z2) → c9(B(z0, b(z1, z2)), B(z1, z2))
B(s(z0), s(z1)) → c12(B(z0, z1))
D'(c(z0, z1)) → c2(D'(z0), D'(z1))
D'(pow(z0, z1)) → c7(D'(z0), D'(z1))

K tuples:none
Defined Rule Symbols:

D, b

Defined Pair Symbols:

D', B

Compound Symbols:

c3, c4, c6, c8, c9, c12, c2, c7

(9) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

D(constant) → h
D(c(z0, z1)) → b(c(z1, D(z0)), c(z0, D(z1)))
D(div(z0, z1)) → m(div(D(z0), z1), div(c(z0, D(z1)), pow(z1, 2)))
D(ln(z0)) → div(D(z0), z0)
D(t) → s(h)
D(m(z0, z1)) → m(D(z0), D(z1))
D(pow(z0, z1)) → b(c(c(z1, pow(z0, m(z1, 1))), D(z0)), c(c(pow(z0, z1), ln(z0)), D(z1)))
D(opp(z0)) → opp(D(z0))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

b(b(z0, z1), z2) → b(z0, b(z1, z2))
b(z0, h) → z0
b(s(z0), s(z1)) → s(s(b(z0, z1)))
b(h, z0) → z0

Tuples:

D'(div(z0, z1)) → c3(D'(z0), D'(z1))
D'(ln(z0)) → c4(D'(z0))
D'(m(z0, z1)) → c6(D'(z0), D'(z1))
D'(opp(z0)) → c8(D'(z0))
B(b(z0, z1), z2) → c9(B(z0, b(z1, z2)), B(z1, z2))
B(s(z0), s(z1)) → c12(B(z0, z1))
D'(c(z0, z1)) → c2(D'(z0), D'(z1))
D'(pow(z0, z1)) → c7(D'(z0), D'(z1))

S tuples:

D'(div(z0, z1)) → c3(D'(z0), D'(z1))
D'(ln(z0)) → c4(D'(z0))
D'(m(z0, z1)) → c6(D'(z0), D'(z1))
D'(opp(z0)) → c8(D'(z0))
B(b(z0, z1), z2) → c9(B(z0, b(z1, z2)), B(z1, z2))
B(s(z0), s(z1)) → c12(B(z0, z1))
D'(c(z0, z1)) → c2(D'(z0), D'(z1))
D'(pow(z0, z1)) → c7(D'(z0), D'(z1))

K tuples:none
Defined Rule Symbols:

b

Defined Pair Symbols:

D', B

Compound Symbols:

c3, c4, c6, c8, c9, c12, c2, c7

(11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

D'(div(z0, z1)) → c3(D'(z0), D'(z1))
D'(ln(z0)) → c4(D'(z0))
D'(m(z0, z1)) → c6(D'(z0), D'(z1))
D'(opp(z0)) → c8(D'(z0))
D'(c(z0, z1)) → c2(D'(z0), D'(z1))

We considered the (Usable) Rules:none
And the Tuples:

D'(div(z0, z1)) → c3(D'(z0), D'(z1))
D'(ln(z0)) → c4(D'(z0))
D'(m(z0, z1)) → c6(D'(z0), D'(z1))
D'(opp(z0)) → c8(D'(z0))
B(b(z0, z1), z2) → c9(B(z0, b(z1, z2)), B(z1, z2))
B(s(z0), s(z1)) → c12(B(z0, z1))
D'(c(z0, z1)) → c2(D'(z0), D'(z1))
D'(pow(z0, z1)) → c7(D'(z0), D'(z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(B(x₁, x₂)) = 0   
POL(D'(x₁)) = x₁   
POL(b(x₁, x₂)) = [1] + x₁   
POL(c(x₁, x₂)) = [1] + x₁ + x₂   
POL(c12(x₁)) = x₁   
POL(c2(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁, x₂)) = x₁ + x₂   
POL(c4(x₁)) = x₁   
POL(c6(x₁, x₂)) = x₁ + x₂   
POL(c7(x₁, x₂)) = x₁ + x₂   
POL(c8(x₁)) = x₁   
POL(c9(x₁, x₂)) = x₁ + x₂   
POL(div(x₁, x₂)) = [1] + x₁ + x₂   
POL(h) = 0   
POL(ln(x₁)) = [1] + x₁   
POL(m(x₁, x₂)) = [1] + x₁ + x₂   
POL(opp(x₁)) = [1] + x₁   
POL(pow(x₁, x₂)) = x₁ + x₂   
POL(s(x₁)) = [1]   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

b(b(z0, z1), z2) → b(z0, b(z1, z2))
b(z0, h) → z0
b(s(z0), s(z1)) → s(s(b(z0, z1)))
b(h, z0) → z0

Tuples:

D'(div(z0, z1)) → c3(D'(z0), D'(z1))
D'(ln(z0)) → c4(D'(z0))
D'(m(z0, z1)) → c6(D'(z0), D'(z1))
D'(opp(z0)) → c8(D'(z0))
B(b(z0, z1), z2) → c9(B(z0, b(z1, z2)), B(z1, z2))
B(s(z0), s(z1)) → c12(B(z0, z1))
D'(c(z0, z1)) → c2(D'(z0), D'(z1))
D'(pow(z0, z1)) → c7(D'(z0), D'(z1))

S tuples:

B(b(z0, z1), z2) → c9(B(z0, b(z1, z2)), B(z1, z2))
B(s(z0), s(z1)) → c12(B(z0, z1))
D'(pow(z0, z1)) → c7(D'(z0), D'(z1))

K tuples:

D'(div(z0, z1)) → c3(D'(z0), D'(z1))
D'(ln(z0)) → c4(D'(z0))
D'(m(z0, z1)) → c6(D'(z0), D'(z1))
D'(opp(z0)) → c8(D'(z0))
D'(c(z0, z1)) → c2(D'(z0), D'(z1))

Defined Rule Symbols:

b

Defined Pair Symbols:

D', B

Compound Symbols:

c3, c4, c6, c8, c9, c12, c2, c7

(13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

B(b(z0, z1), z2) → c9(B(z0, b(z1, z2)), B(z1, z2))

We considered the (Usable) Rules:none
And the Tuples:

D'(div(z0, z1)) → c3(D'(z0), D'(z1))
D'(ln(z0)) → c4(D'(z0))
D'(m(z0, z1)) → c6(D'(z0), D'(z1))
D'(opp(z0)) → c8(D'(z0))
B(b(z0, z1), z2) → c9(B(z0, b(z1, z2)), B(z1, z2))
B(s(z0), s(z1)) → c12(B(z0, z1))
D'(c(z0, z1)) → c2(D'(z0), D'(z1))
D'(pow(z0, z1)) → c7(D'(z0), D'(z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(B(x₁, x₂)) = [3] + [2]x₁   
POL(D'(x₁)) = 0   
POL(b(x₁, x₂)) = [2] + [2]x₁ + [2]x₂   
POL(c(x₁, x₂)) = 0   
POL(c12(x₁)) = x₁   
POL(c2(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁, x₂)) = x₁ + x₂   
POL(c4(x₁)) = x₁   
POL(c6(x₁, x₂)) = x₁ + x₂   
POL(c7(x₁, x₂)) = x₁ + x₂   
POL(c8(x₁)) = x₁   
POL(c9(x₁, x₂)) = x₁ + x₂   
POL(div(x₁, x₂)) = 0   
POL(h) = 0   
POL(ln(x₁)) = 0   
POL(m(x₁, x₂)) = 0   
POL(opp(x₁)) = 0   
POL(pow(x₁, x₂)) = 0   
POL(s(x₁)) = x₁   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

b(b(z0, z1), z2) → b(z0, b(z1, z2))
b(z0, h) → z0
b(s(z0), s(z1)) → s(s(b(z0, z1)))
b(h, z0) → z0

Tuples:

D'(div(z0, z1)) → c3(D'(z0), D'(z1))
D'(ln(z0)) → c4(D'(z0))
D'(m(z0, z1)) → c6(D'(z0), D'(z1))
D'(opp(z0)) → c8(D'(z0))
B(b(z0, z1), z2) → c9(B(z0, b(z1, z2)), B(z1, z2))
B(s(z0), s(z1)) → c12(B(z0, z1))
D'(c(z0, z1)) → c2(D'(z0), D'(z1))
D'(pow(z0, z1)) → c7(D'(z0), D'(z1))

S tuples:

B(s(z0), s(z1)) → c12(B(z0, z1))
D'(pow(z0, z1)) → c7(D'(z0), D'(z1))

K tuples:

D'(div(z0, z1)) → c3(D'(z0), D'(z1))
D'(ln(z0)) → c4(D'(z0))
D'(m(z0, z1)) → c6(D'(z0), D'(z1))
D'(opp(z0)) → c8(D'(z0))
D'(c(z0, z1)) → c2(D'(z0), D'(z1))
B(b(z0, z1), z2) → c9(B(z0, b(z1, z2)), B(z1, z2))

Defined Rule Symbols:

b

Defined Pair Symbols:

D', B

Compound Symbols:

c3, c4, c6, c8, c9, c12, c2, c7

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

B(s(z0), s(z1)) → c12(B(z0, z1))

We considered the (Usable) Rules:none
And the Tuples:

D'(div(z0, z1)) → c3(D'(z0), D'(z1))
D'(ln(z0)) → c4(D'(z0))
D'(m(z0, z1)) → c6(D'(z0), D'(z1))
D'(opp(z0)) → c8(D'(z0))
B(b(z0, z1), z2) → c9(B(z0, b(z1, z2)), B(z1, z2))
B(s(z0), s(z1)) → c12(B(z0, z1))
D'(c(z0, z1)) → c2(D'(z0), D'(z1))
D'(pow(z0, z1)) → c7(D'(z0), D'(z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(B(x₁, x₂)) = [1] + x₁   
POL(D'(x₁)) = 0   
POL(b(x₁, x₂)) = [2] + x₁ + [2]x₂   
POL(c(x₁, x₂)) = 0   
POL(c12(x₁)) = x₁   
POL(c2(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁, x₂)) = x₁ + x₂   
POL(c4(x₁)) = x₁   
POL(c6(x₁, x₂)) = x₁ + x₂   
POL(c7(x₁, x₂)) = x₁ + x₂   
POL(c8(x₁)) = x₁   
POL(c9(x₁, x₂)) = x₁ + x₂   
POL(div(x₁, x₂)) = 0   
POL(h) = 0   
POL(ln(x₁)) = 0   
POL(m(x₁, x₂)) = 0   
POL(opp(x₁)) = 0   
POL(pow(x₁, x₂)) = 0   
POL(s(x₁)) = [1] + x₁   

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

b(b(z0, z1), z2) → b(z0, b(z1, z2))
b(z0, h) → z0
b(s(z0), s(z1)) → s(s(b(z0, z1)))
b(h, z0) → z0

Tuples:

D'(div(z0, z1)) → c3(D'(z0), D'(z1))
D'(ln(z0)) → c4(D'(z0))
D'(m(z0, z1)) → c6(D'(z0), D'(z1))
D'(opp(z0)) → c8(D'(z0))
B(b(z0, z1), z2) → c9(B(z0, b(z1, z2)), B(z1, z2))
B(s(z0), s(z1)) → c12(B(z0, z1))
D'(c(z0, z1)) → c2(D'(z0), D'(z1))
D'(pow(z0, z1)) → c7(D'(z0), D'(z1))

S tuples:

D'(pow(z0, z1)) → c7(D'(z0), D'(z1))

K tuples:

D'(div(z0, z1)) → c3(D'(z0), D'(z1))
D'(ln(z0)) → c4(D'(z0))
D'(m(z0, z1)) → c6(D'(z0), D'(z1))
D'(opp(z0)) → c8(D'(z0))
D'(c(z0, z1)) → c2(D'(z0), D'(z1))
B(b(z0, z1), z2) → c9(B(z0, b(z1, z2)), B(z1, z2))
B(s(z0), s(z1)) → c12(B(z0, z1))

Defined Rule Symbols:

b

Defined Pair Symbols:

D', B

Compound Symbols:

c3, c4, c6, c8, c9, c12, c2, c7

(17) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

D'(pow(z0, z1)) → c7(D'(z0), D'(z1))

We considered the (Usable) Rules:none
And the Tuples:

D'(div(z0, z1)) → c3(D'(z0), D'(z1))
D'(ln(z0)) → c4(D'(z0))
D'(m(z0, z1)) → c6(D'(z0), D'(z1))
D'(opp(z0)) → c8(D'(z0))
B(b(z0, z1), z2) → c9(B(z0, b(z1, z2)), B(z1, z2))
B(s(z0), s(z1)) → c12(B(z0, z1))
D'(c(z0, z1)) → c2(D'(z0), D'(z1))
D'(pow(z0, z1)) → c7(D'(z0), D'(z1))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(B(x₁, x₂)) = 0   
POL(D'(x₁)) = x₁   
POL(b(x₁, x₂)) = [1] + x₁   
POL(c(x₁, x₂)) = [1] + x₁ + x₂   
POL(c12(x₁)) = x₁   
POL(c2(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁, x₂)) = x₁ + x₂   
POL(c4(x₁)) = x₁   
POL(c6(x₁, x₂)) = x₁ + x₂   
POL(c7(x₁, x₂)) = x₁ + x₂   
POL(c8(x₁)) = x₁   
POL(c9(x₁, x₂)) = x₁ + x₂   
POL(div(x₁, x₂)) = [1] + x₁ + x₂   
POL(h) = 0   
POL(ln(x₁)) = x₁   
POL(m(x₁, x₂)) = x₁ + x₂   
POL(opp(x₁)) = x₁   
POL(pow(x₁, x₂)) = [1] + x₁ + x₂   
POL(s(x₁)) = [1]   

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

b(b(z0, z1), z2) → b(z0, b(z1, z2))
b(z0, h) → z0
b(s(z0), s(z1)) → s(s(b(z0, z1)))
b(h, z0) → z0

Tuples:

D'(div(z0, z1)) → c3(D'(z0), D'(z1))
D'(ln(z0)) → c4(D'(z0))
D'(m(z0, z1)) → c6(D'(z0), D'(z1))
D'(opp(z0)) → c8(D'(z0))
B(b(z0, z1), z2) → c9(B(z0, b(z1, z2)), B(z1, z2))
B(s(z0), s(z1)) → c12(B(z0, z1))
D'(c(z0, z1)) → c2(D'(z0), D'(z1))
D'(pow(z0, z1)) → c7(D'(z0), D'(z1))

S tuples:none
K tuples:

D'(div(z0, z1)) → c3(D'(z0), D'(z1))
D'(ln(z0)) → c4(D'(z0))
D'(m(z0, z1)) → c6(D'(z0), D'(z1))
D'(opp(z0)) → c8(D'(z0))
D'(c(z0, z1)) → c2(D'(z0), D'(z1))
B(b(z0, z1), z2) → c9(B(z0, b(z1, z2)), B(z1, z2))
B(s(z0), s(z1)) → c12(B(z0, z1))
D'(pow(z0, z1)) → c7(D'(z0), D'(z1))

Defined Rule Symbols:

b

Defined Pair Symbols:

D', B

Compound Symbols:

c3, c4, c6, c8, c9, c12, c2, c7

(19) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty

(20) BOUNDS(1, 1)